x:chain_master(). (cmseq?(x))  (cmseq-from(x)  Id) 

latex

Definitions	if b then t else f fi , tt, ff, cmseq-from(x), t  T, cmseq?(x), b, P  Q, x:A. B(x), False, chain_master(), cmseq(from;to;num), , cmconfig(list)
Lemmas	chain master wf, cmseq? wf, assert wf, true wf, false wf